es:ES, P:(E).
(e:E. Dec(P(e)))
 (e:E.
 (e':E. ((e' < e) & P(e')))
  (e':E. ((e' < e) & P(e') & (e'':E. (e' < e'')  (e'' < e)  (P(e'')))))) 

latex

Definitions

x:A  B(x), x:A. B(x), x:AB(x), x:A. B(x), s = t, t  T, strong-subtype(A;B), P  Q, f(a), ES, Dec(P), left + right, P  Q, False, A, P  Q, a < b, A  B, b, {i..j}, b | a, a ~ b, a  b, a <p b, a < b, A c B, x f y, xL. P(x), (xL.P(x)), R^+, r  s, r < s, q-rel(r;x), type List, Outcome, (x  l), l_disjoint(T;l1;l2), (e <loc e'), e loc e' , e c e', e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), Type, , SWellFounded(R(x;y)), x,y. t(x;y), x(s), (e < e'), P & Q, x.A(x), E, R1 => R2, {T}, x:A.B(x), x. t(x), Void, R!

Lemmas

false wf, decidable existse-causl, decidable cand, decidable es-causl, member wf, strongwf-monotone, rel implies wf, es-causl-swellfnd, event system wf, not wf, es-causl wf, rel-immediate-exists, strongwellfounded wf, es-E wf, decidable wf